William Retert, Ph.D.
Instructor
- Milwaukee WI UNITED STATES
- Diercks Hall DH428
- Electrical Engineering and Computer Science
Dr. William Retert is an expert in the areas of computer science and software engineering.
Education, Licensure and Certification
Ph.D.
University of Wisconsin-Milwaukee
Computer Science Engineering
2009
M.S.
University of Wisconsin-Milwaukee
Computer Science
2000
B.S.
University of Wisconsin-Milwaukee
Mathematics
1997
Biography
Areas of Expertise
Selected Publications
Connecting Effects and Uniqueness With Adoption
ACM SIGPLANBoyland, J. T., Retert, W.
2005
"Adoption" is when on piece of stat is logically embedded in another piece of state. Adoption provides information hiding (the adopter can be used as a proxy for the adoptee) and with linear existentials, provides a way to store unique pointers in shared state. In this paper, we give an operational semantics of adoption in a simple procedural language with pointers to records. We define a "permission" type-system that uses adoption to model both effects and uniqueness. We prove type soundness (well-typed programs don't go wrong) and state separation (separately-typed statements cannot access the same state). Then we show how high-level effects and uniqueness annotations can be expressed in the type-system. The distinction between read and write effects is ignored in the body of this paper.
Interprocedural Analysis for JVML Verification
Proceedings of the 4th ECOOP Workshop on Formal Techniques for Java-like ProgramRetert, W., Boyland, J.
2002
Some of the problems encountered in the verification of subroutines in the Java Virtual Machine Language (JVML) are similar to problems already solved for interprocedural analysis in high question of whether techniques for the latter may be successfully applied to the former. To this end, we apply a general framework for interprocedural abstract interpretation to JVML0, a subset of JVML that isolates subroutines
